A, B:System, i:Id. (j:Id. j = i  A(j) =   MsgA)  A(i)  B(i)  s-dsys(A)  s-dsys(B) 

latex

Definitions	Id, D1  D2, A, Prop, , MsgA, Feasible(M), P  Q, System, M1  M2, x:A. B(x), Dec(P), P  Q, t  T
Lemmas	decidable equal Id, s-dsys-sub-s-dsys, ma-feasible wf, Id wf, msga wf, ma-empty wf, not wf, ma-sub wf, ma-empty-sub